home *** CD-ROM | disk | FTP | other *** search
/ Freaks Macintosh Archive / Freaks Macintosh Archive.bin / Freaks Macintosh Archives / Textfiles / coloredbooks / PurpleBook.sit.hqx / Purple Book
Text File  |  1997-11-17  |  56KB  |  1,610 lines
  1.  
  2.  
  3.  
  4.  
  5.  
  6.  
  7.  
  8. Guidelines for Formal Verification Systems
  9.  
  10.  
  11.  
  12.  
  13.  
  14.  
  15. NCSC-TG-014-89
  16.  
  17.  
  18. Library No.  S-231,308
  19. Guidelines for Formal Verification Systems
  20.  
  21. FOREWORD
  22.  
  23.  
  24.  
  25. This publication, Guidelines for Formal Verification Systems,
  26. is issued by the National Computer Security Center (NCSC) under
  27. the authority and in accordance with Department of Defense (DoD)
  28. Directive 5215.1, "Computer Security Evaluation Center."
  29.  The guidelines defined in this document are intended for vendors
  30. building formal specification and verification systems that trusted
  31. system developers may use in satisfying the requirements of the
  32. Department of Defense Trusted Computer System Evaluation Criteria
  33. (TCSEC), DoD 5200.28-STD, and the Trusted Network Interpretation
  34. of the TCSEC.
  35.  
  36.  
  37. As the Director, National Computer Security Center, I invite your
  38. recommendations for revision to this technical guideline.  Address
  39. all proposals for revision through appropriate channels to the
  40. National Computer Security Center, 9800 Savage Road, Fort George
  41. G.  Meade, MD, 20755-6000, Attention: Chief, Technical Guidelines
  42. Division.
  43.  
  44.  
  45. Patrick R.  Gallagher, Jr.
  46.  
  47.  
  48. 1 April 1989
  49.  
  50.  • Director
  51.  • National Computer Security Center
  52.  
  53.  
  54.  
  55.  
  56.  
  57. ACKNOWLEDGMENTS
  58.  
  59.  
  60.  
  61. The National Computer Security Center expresses appreciation to
  62. Barbara Mayer and Monica McGill Lu as principal authors and project
  63. managers of this document.  We recognize their contribution to
  64. the technical content and presentation of this publication.
  65.  
  66.  
  67. We thank the many individuals who contributed to the concept,
  68. development, and review of this document.  In particular, we acknowledge:
  69.  Karen Ambrosi, Tom Ambrosi, Terry Benzel, David Gibson, Sandra
  70. Goldston, Dale Johnson, Richard Kemmerer, Carl Landwehr, Carol
  71. Lane, John McLean, Jonathan Millen, Andrew Moore, Michele Pittelli,
  72. Marvin Schaefer, Michael Sebring, Jeffrey Thomas, Tom Vander-Vlis,
  73. Alan Whitehurst, James Williams, Kimberly Wilson, and Mark Woodcock.
  74.  Additionally, we thank the verification system developers and
  75. the rest of the verification community who helped develop this
  76. document.
  77. PREFACE
  78.  
  79.  
  80.  
  81. One of the goals of the NCSC is to encourage the development of
  82. production-quality verification systems.  This guideline was developed
  83. as part of the Technical Guideline Program specifically to support
  84. this goal.
  85.  
  86.  
  87. Although there are manual methodologies for performing formal
  88. specification and verification, this guideline addresses verification
  89. systems that provide automated support.
  90.  
  91.  
  92. Throughout the document, the term developer is used to describe
  93. the developer of the verification system.  The term vendor is
  94. used to describe the individual(s) who are providing support for
  95. the tool.  These individuals may or may not be the same for a
  96. particular tool.
  97. 1. INTRODUCTION
  98.  
  99.  
  100.  
  101. The principal goal of the National Computer Security Center (NCSC)
  102. is to encourage the widespread availability of trusted computer
  103. systems.  In support of this goal the DoD Trusted Computer System
  104. Evaluation Criteria (TCSEC) was created, against which computer
  105. systems could be evaluated.  The TCSEC was originally published
  106. on 15 August 1983 as CSC-STD-001-83. 
  107.  
  108.  
  109. In December 1985 the DoD modified and adopted the TCSEC as a DoD
  110. Standard,
  111.  
  112.  
  113. DoD 5200.28-STD. [1]
  114. 1.1 PURPOSE
  115.  
  116.  
  117.  
  118. This document explains the requirements for formal verification
  119. systems that are candidates for the NCSC's Endorsed Tools List
  120. (ETL). [5]  This document is primarily intended for developers
  121. of verification systems to use in the development of production-quality
  122. formal verification systems.  It explains the requirements and
  123. the process used to evaluate formal verification systems submitted
  124. to the NCSC for endorsement.
  125. 1.2 BACKGROUND
  126.  
  127.  
  128.  
  129. The requirement for NCSC endorsement of verification systems is
  130. stated in the TCSEC and the Trusted Network Interpretation of
  131. the TCSEC (TNI). [4]  The TCSEC and TNI are the standards used
  132. for evaluating security controls built into automated information
  133. and network systems, respectively.  The TCSEC and TNI classify
  134. levels of trust for computer and network systems by defining divisions
  135. and classes within divisions.  Currently, the most trusted class
  136. defined is A1, Verified Design, which requires formal design specification
  137. and formal verification.  As stated in the TCSEC and TNI, ".
  138. . . verification evidence shall be consistent with that provided
  139. within the state of the art of the particular Computer Security
  140. Center-endorsed formal specification and verification system used."
  141. [1]
  142.  
  143.  
  144. Guidelines were not available when the NCSC first considered endorsing
  145. verification systems.  The NCSC based its initial endorsement
  146. of verification systems on support and maintenance of the system,
  147. acceptance within the verification community, and stability of
  148. the system.
  149. 1.3 SCOPE
  150.  
  151.  
  152.  
  153. Any verification system that has the capability for formally specifying
  154. and verifying the design of a trusted system to meet the TCSEC
  155. and TNI A1 Design Specification and Verification requirement can
  156. be considered for placement on the ETL.  Although verification
  157. systems that have capabilities beyond design verification are
  158. highly encouraged by the NCSC, this guideline focuses mainly on
  159. those aspects of verification systems that are sufficient for
  160. the design of candidate A1 systems.
  161.  
  162.  
  163. The requirements described in this document are the primary consideration
  164. in the endorsement process.  They are categorized as either methodology
  165. and system specification or implementation and other support factors.
  166.  Within each category are requirements for features, assurances,
  167. and documentation. 
  168.  
  169.  
  170. The requirements cover those characteristics that can and should
  171. exist in current verification technology for production-quality
  172. systems.  A production-quality verification system is one that
  173. is sound, user-friendly, efficient, robust, well documented, maintainable,
  174. developed with good software engineering techniques, and available
  175. on a variety of hardware. [2]  The NCSC's goal is to elevate the
  176. current state of  verification technology to production quality,
  177. while still encouraging the advancement of research in the verification
  178. field.
  179.  
  180.  
  181. Since the NCSC is limited in resources for both evaluation and
  182. support of verification systems, the ETL may reflect this limitation.
  183.  Verification systems placed on the ETL will either be significant
  184. improvements to systems already on the list or will provide a
  185. useful approach or capability that the currently endorsed systems
  186. lack.
  187.  
  188.  
  189. This guideline was written to help in identifying the current
  190. needs in verification systems and to encourage future growth of
  191. verification technology.  The evaluation process is described
  192. in the following section.  Verification systems will be evaluated
  193. against the requirements listed in sections 3 and 4.  Section
  194. 5 contains a short list of possibilities for next-generation verification
  195. systems.  It is not an all-encompassing list of features as this
  196. would be counterproductive to the goals of research.
  197. 2. EVALUATION APPROACH
  198.  
  199.  
  200.  
  201. A formal request for evaluation of a verification system for placement
  202. on the ETL shall be submitted in writing directly to:
  203.  
  204.  
  205. National Computer Security Center
  206.  
  207.  
  208.     ATTN:  Deputy
  209.  
  210.  
  211. C (Verification Committee Chairperson)
  212.  
  213.  
  214. 9800 Savage Road
  215.  
  216.  
  217. Fort George G. Meade, MD 20755-6000
  218.  
  219.  
  220. Submitting a verification system does not guarantee NCSC evaluation
  221. or placement on the ETL.
  222.  
  223.  
  224. The developers shall submit a copy of the verification system
  225. to the NCSC along with supporting documentation and tools, test
  226. suites, configuration management evidence, and source code.  In
  227. addition, the system developers shall support the NCSC evaluators.
  228.  For example, the developers shall be available to answer questions,
  229. provide training, and meet with the evaluation team.
  230.  
  231.  
  232. There are three cases in which an evaluation can occur:  1) the
  233. evaluation of a new verification system being considered for placement
  234. on the ETL, 2) the reevaluation of a new version of a system already
  235. on the ETL for placement on the ETL (reevaluation for endorsement),
  236. and 3) the reevaluation of a system on the ETL being considered
  237. for removal from the ETL (reevaluation for removal).
  238. 2.1 EVALUATION OF NEW SYSTEMS
  239.  
  240.  
  241.  
  242. To be considered for initial placement on the ETL, the candidate
  243. endorsed tool must provide some significant feature or improvement
  244. that is not available in any of the currently endorsed tools.
  245.  If the verification system meets this requirement, the evaluators
  246. shall analyze the entire verification system, concentrating on
  247. the requirements described in Chapters 3 and 4 of this document.
  248.  If a requirement is not completely satisfied, but the developer
  249. is working toward completion, the relative significance of the
  250. requirement shall be measured by the evaluation team.  The team
  251. shall determine if the deficiency is substantial or detrimental.
  252.  For example, a poor user interface would not be as significant
  253. as the lack of a justification of the methodology.  Requirements
  254. not completely satisfied shall be identified and documented in
  255. the final evaluation report.
  256.  
  257.  
  258. Studies or prior evaluations (e.g., the Verification Assessment
  259. Study Final Report) [2] performed on the verification system shall
  260. be reviewed.  Strengths and weaknesses identified in other reports
  261. shall be considered when evaluating the verification system.
  262.  
  263.  
  264. The following are the major steps leading to an endorsement and
  265. ETL listing for a new verification system.
  266.  
  267.  • 1) The developer submits a request for evaluation to the NCSC
  268. Verification Committee Chairperson.
  269.  • 2) The Committee meets to determine whether the verification
  270. system provides a significant improvement to systems already on
  271. the ETL or provides a useful approach or capability that the existing
  272. systems lack.
  273.  • 3) If the result is favorable, an evaluation team is formed
  274. and the verification system evaluation begins.
  275.  • 4) Upon completion of the evaluation, a Technical
  276.  
  277.  
  278.  
  279.  
  280. Assessment Report (TAR) is written by the evaluation team.
  281.  
  282.  • 5) The Committee reviews the TAR and makes recommendations
  283. on endorsement.
  284.  • 6) The Committee Chairperson approves or disapproves endorsement.
  285.  • 7) If approved, an ETL entry is issued for the verification
  286. system.
  287.  • 8) A TAR is issued for the verification system.
  288.  
  289.  
  290.  
  291.  
  292.  
  293. 2.2 REEVALUATION FOR ENDORSEMENT
  294.  
  295.  
  296.  
  297. The term reevaluation for endorsement denotes the evaluation of
  298. a new version of an endorsed system for placement on the ETL.
  299.  A significant number of changes or enhancements, as determined
  300. by the developer, may warrant a reevaluation for endorsement.
  301.  The intent of this type of reevaluation is to permit improvements
  302. to endorsed versions and advocate state-of-the-art technology
  303. on the ETL while maintaining the assurance of the original endorsed
  304. version. 
  305.  
  306.  
  307. A verification system that is already on the ETL maintains assurance
  308. of soundness and integrity through configuration management (see
  309. Appendix).  The documentation of this process is evidence for
  310. the reevaluation of the verification system.  Reevaluations are
  311. based upon an assessment of all evidence and a presentation of
  312. this material by the vendor to the NCSC.  The NCSC reserves the
  313. right to request additional evidence as necessary.
  314.  
  315.  
  316. The vendor shall prepare the summary of evidence in the form of
  317. a Vendor Report (VR).  The vendor may submit the VR to the NCSC
  318. at any time after all changes have ended for the version in question.
  319.  The VR shall relate the reevaluation evidence at a level of detail
  320. equivalent to the TAR.  The VR shall assert that assurance has
  321. been upheld and shall include sufficient commentary to allow an
  322. understanding of every change made to the verification system
  323. since the endorsed version. 
  324.  
  325.  
  326. The Committee shall expect the vendor to present a thorough technical
  327. overview of changes to the verification system and an analysis
  328. of the changes, demonstrating continuity and retention of assurance.
  329.  The Committee subsequently issues a recommendation to the Committee
  330. Chairperson stating that assurance has or has not been maintained
  331. by the current verification system since it was endorsed.  If
  332. the verification system does not sustain its endorsement, the
  333. vendor may be given the option for another review by the Committee.
  334.  The reevaluation cycle ends with an endorsement determination
  335. by the Committee Chairperson, and if the determination is favorable,
  336. a listing of the new release is added to the ETL, replacing the
  337. previously endorsed version; the old version is then archived.
  338.  
  339.  
  340. The following are the major steps leading to an endorsement and
  341. ETL listing for a revised verification system.
  342.  
  343.  • 1) The vendor submits the VR and other materials to the NCSC
  344. Verification Committee Chairperson.
  345.  • 2) An evaluation team is formed to review the VR.
  346.  • 3) The team adds any additional comments and submits them
  347. to the Verification Committee.
  348.  • 4) The vendor defends the VR before the Committee.
  349.  • 5) The Committee makes recommendations on endorsement.
  350.  • 6) The Committee Chairperson approves or disapproves endorsement.
  351.  • 7) If approved, a new ETL entry is issued for the revised
  352. verification system.
  353.  • 8) The VR is issued for the revised verification system.
  354.  
  355.  
  356.  
  357.  
  358.  
  359. 2.3 REEVALUATION FOR REMOVAL
  360.  
  361.  
  362.  
  363. Once a verification system is endorsed, it shall normally remain
  364. on the ETL as long as it is supported and is not replaced by another
  365. system.  The Committee makes the final decision on removal of
  366. a verification system from the ETL.  For example, too many bugs,
  367. lack of users, elimination of support and maintenance, and unsoundness
  368. are all reasons which may warrant removal of a verification system
  369. from the ETL.  Upon removal, the Committee makes a formal announcement
  370. and provides a written justification of their decision. 
  371.  
  372.  
  373. Systems on the ETL that are removed or replaced shall be archived.
  374.  Systems developers that have a Memorandum of Agreement (MOA)
  375. with the NCSC to use a verification system that is later archived
  376. may continue using the system agreed upon in the MOA.  Verification
  377. evidence from a removed or replaced verification system shall
  378. not be accepted in new system evaluations for use in satisfying
  379. the A1 Design Specification and Verification requirement.
  380.  
  381.  
  382. The following are the major steps leading to the removal of a
  383. verification system from the ETL.
  384.  
  385.  • 1) The Verification Committee questions the endorsement of
  386. a verification system on the ETL.
  387.  • 2) An evaluation team is formed and the verification system
  388. evaluation begins, focusing on the area in question.
  389.  • 3) Upon completion of the evaluation, a TAR is written by
  390. the evaluation team.
  391.  • 4) The Committee reviews the TAR and makes recommendations
  392. on removal.
  393.  • 5) The Committee Chairperson approves or disapproves removal.
  394.  • 6) If removed, a new ETL is issued eliminating the verification
  395. system in question.
  396.  • 7) A TAR is issued for the verification system under evaluation.
  397.  
  398.  
  399.  
  400.  
  401.  
  402. 2.4 BETA VERSIONS
  403.  
  404.  
  405.  
  406. Currently, verification systems are not production quality tools
  407. and are frequently being enhanced and corrected.  The version
  408. of a verification system that has been endorsed may not be the
  409. newest and most capable version.  Modified versions are known
  410. as beta tool versions.  Beta versions are useful in helping system
  411. developers uncover bugs before submitting the verification system
  412. for evaluation.
  413.  
  414.  
  415. The goal of beta versions is to stabilize the verification system.
  416.  Users should not assume that any particular beta version will
  417. be evaluated or endorsed by the NCSC.  If the developer of a trusted
  418. system is using a beta version of a formal verification system,
  419. specifications and proof evidence shall be submitted to the NCSC
  420. which can be completely checked without significant modification
  421. using an endorsed tool as stated in the A1 requirement.  This
  422. can be accomplished by using either the currently endorsed version
  423. of a verification system or a previously endorsed version that
  424. was agreed upon by the trusted system developer and the developer's
  425. evaluation team.  Submitted specifications and proof evidence
  426. that are not compatible with the endorsed or agreed-upon version
  427. of the tool may require substantial modification by the trusted
  428. system developer.
  429. 3. METHODOLOGY AND SYSTEM SPECIFICATION
  430.  
  431.  
  432.  
  433. The technical factors listed in this Chapter are useful measures
  434. of the quality and completeness of a verification system.  The
  435. factors are divided into four categories: 1) methodology, 2) features,
  436. 3) assurance, and 4) documentation.  Methodology is the underlying
  437. principles and rules of organization of the verification system.
  438.  Features include the functionality of the verification system.
  439.  Assurance is the confidence and level of trust that can be placed
  440. in the verification system.  Documentation consists of a set of
  441. manuals and technical papers that fully describe the verification
  442. system, its components, application, operation, and maintenance.
  443.  
  444.  
  445. These categories extend across each of the components of the verification
  446. system.  These components minimally consist of the following:
  447.  
  448.  • a) a mathematical specification language that allows the user
  449. to express correctness conditions,
  450.  • b) a specification processor that interprets the specification
  451. and generates conjectures interpretable by the reasoning mechanism,
  452. and
  453.  • c) a reasoning mechanism that interprets the conjectures generated
  454. by the processor and checks the proof or proves that the correctness
  455. conditions are satisfied.
  456.  
  457.  
  458.  
  459.  
  460.  
  461. 3.1 METHODOLOGY
  462.  
  463.  
  464.  
  465. The methodology of the verification system shall consist of a
  466. set of propositions used as rules for performing formal verification
  467. in that system.  This methodology shall have a sound, logical
  468. basis.  This requirement is a necessary but not sufficient condition
  469. for the endorsement of the system.
  470. 3.2 FEATURES
  471.  
  472. 3.2.1 Specification Language
  473.  
  474. a. Language expressiveness.
  475.  
  476.  
  477.  
  478. The specification language shall be sufficiently expressive to
  479. support the methodology of the verification system.  This ensures
  480. that the specification language is powerful and rich enough to
  481. support the underlying methodology.  For example, if the methodology
  482. requires that a specification language be used to model systems
  483. as state machines, then the specification language must semantically
  484. and syntactically support all of the necessary elements for modeling
  485. systems as state machines. 
  486. b. Defined constructs.
  487.  
  488.  
  489.  
  490. The specification language shall consist of a set of constructs
  491. that are rigorously defined (e.g., in Backus-Naur Form with appropriate
  492. semantic definitions).  This implies that the language is formally
  493. described by a set of rules for correct use.
  494. c. Mnemonics.
  495.  
  496.  
  497.  
  498. The syntax of the specification language shall be clear and concise
  499. without obscuring the interpretation of the language constructs.
  500.  Traditional symbols from mathematics should be employed wherever
  501. possible; reasonably mnemonic symbols should be used in other
  502. cases.  This aids the users in interpreting constructs more readily.
  503. d. Internal uniformity.
  504.  
  505.  
  506.  
  507. The syntax of the specification language shall be internally uniform.
  508.  This ensures that the rules of the specification language are
  509. not contradictory.
  510. e. Overloading.
  511.  
  512.  
  513.  
  514. Each terminal symbol of the specification language's grammar should
  515. support one and only one semantic definition insofar as it increases
  516. comprehensibility.  When it is beneficial to incorporate more
  517. than one definition for a symbol or construct, the semantics of
  518. the construct shall be clearly defined from the context used.
  519.  This is necessary to avoid confusion by having one construct
  520. with more than one interpretation or more than one construct with
  521. the same interpretation.  For example, the symbol "+"
  522. may be used for both integer and real addition, but it should
  523. not be used to denote both integer addition and conjunction.
  524. f. Correctness conditions.
  525.  
  526.  
  527.  
  528. The specification language shall provide the capability to express
  529. correctness conditions.
  530. g. Incremental verification.
  531.  
  532.  
  533.  
  534. The methodology shall allow incremental verification. 
  535.  
  536.  
  537. This would allow, for example, a verification of portions of a
  538. system specification at a single time.  Incremental verification
  539. may also include the capability for performing verification of
  540. different levels of abstraction.  This allows essential elements
  541. to be presented in the most abstract level and important details
  542. to be presented at successive levels of refinement.
  543. 3.2.2 Specification Processing
  544.  
  545. a. Input.
  546.  
  547.  
  548.  
  549. All of the constructs of the specification language shall be processible
  550. by the specification processor(s).  This is necessary to convert
  551. the specifications to a language or form that is interpretable
  552. by the reasoning mechanism.
  553. b. Output.
  554.  
  555.  
  556.  
  557. The output from the processor(s) shall be interpretable by the
  558. reasoning mechanism.  Conjectures derived from the correctness
  559. conditions shall be generated.  The output shall also report errors
  560. in specification processing to the user in an easily interpretable
  561. manner.
  562.  
  563.  
  564. Reasoning Mechanism  
  565. 3.2.3 Reasoning Mechanism
  566.  
  567. a. Compatibility of components.
  568.  
  569.  
  570.  
  571. The reasoning mechanism shall be compatible with the other components
  572. of the verification system to ensure that the mechanism is capable
  573. of determining the validity of conjectures produced by other components
  574. of the verification system.  For example, if conjectures are generated
  575. by the specification processor that must be proven, then the reasoning
  576. mechanism must be able to interpret these conjectures correctly.
  577. b. Compatibility of constructs.
  578.  
  579.  
  580.  
  581. The well-formed formulas in the specification language that may
  582. also be input either directly or indirectly into the reasoning
  583. mechanism using the language(s) of the reasoning mechanism shall
  584. be mappable to ensure compatibility of components.  For example,
  585. if a lemma can be defined in the specification language as "LEMMA
  586. <well-formed formula>" and can also be defined in the
  587. reasoning mechanism, then the construct for the lemma in the reasoning
  588. mechanism shall be in the same form.
  589. c. Documentation.
  590.  
  591.  
  592.  
  593. The reasoning mechanism shall document the steps it takes to develop
  594. the proof.  Documentation provides users with a stable, standard
  595. reasoning mechanism that facilitates debugging and demonstrates
  596. completed proofs.  If the reasoning mechanism is defined to use
  597. more than one method of reasoning, then it should clearly state
  598. which method is used and remain consistent within each method
  599. of reasoning.
  600. d. Reprocessing.
  601.  
  602.  
  603.  
  604. The reasoning mechanism shall provide a means for reprocessing
  605. completed proof sessions.  This is to ensure that users have a
  606. means of reprocessing theorems without reconstructing the proof
  607. process.  This mechanism shall also save the users from reentering
  608. voluminous input to the reasoning mechanism.  For example, reprocessing
  609. may be accomplished by the generation of command files that can
  610. be invoked to recreate the proof session.
  611. e. Validation.
  612.  
  613.  
  614.  
  615. The methodology shall provide a means for validating proof sessions
  616. independently of the reasoning mechanism.  Proof strategies checked
  617. by an independent, trustworthy proof checker shall ensure that
  618. only sound proof steps were employed in the proof process.  Trustworthy
  619. implies that there is assurance that the proof checker accepts
  620. only valid proofs.  The validation process shall not be circumventable
  621. and shall always be invoked for each completed proof session.
  622. f. Reusability.
  623.  
  624.  
  625.  
  626. The reasoning mechanism shall facilitate the use of system- and
  627. user-supplied databases of reusable definitions and theorems.
  628.  This provides a foundation for proof sessions that will save
  629. the user time and resources in reproving similar theorems and
  630. lemmas.
  631. g. Proof dependencies.
  632.  
  633.  
  634.  
  635. The reasoning mechanism shall track the status of the use and
  636. reuse of theorems throughout all phases of development.  Proof
  637. dependencies shall be identified and maintained so that if modifications
  638. are made to a specification (and indirectly to any related conjectures/theorems),
  639. the minimal set of theorems and lemmas that are dependent on the
  640. modified proofs will need to be reproved.
  641. 3.3 ASSURANCE, SOUNDNESS, AND ROBUSTNESS
  642.  
  643. a. Sound basis.
  644.  
  645.  
  646.  
  647. Each of the verification system's tools and services shall support
  648. the method*ology.  This ensures that users can understand the
  649. functionality of the verification system with respect to the methodology
  650. and that the methodology is supported by the components of the
  651. verification system.
  652. b. Correctness.
  653.  
  654.  
  655.  
  656. The verification system shall be rigorously tested to provide
  657. assurance that the majority of the system is free of error.
  658. c. Predictability.
  659.  
  660.  
  661.  
  662. The verification system shall behave predictably.  Consistent
  663. results are  needed for the users to interpret the results homogeneously.
  664.  This will ensure faster and easier interpretation and fewer errors
  665. in interpretation. 
  666. d. Previous use.
  667.  
  668.  
  669.  
  670. The verification system shall have a history of use to establish
  671. stability, usefulness, and credibility.  This history shall contain
  672. documentation of applications (for example, applications from
  673. academia or the developers).  These applications shall test the
  674. verification system, so that strengths and weaknesses may be uncovered.
  675. e. Error recovery.
  676.  
  677.  
  678.  
  679. The verification system shall gracefully recover from internal
  680. software errors.  This error handling is necessary to ensure that
  681. errors in the verification system do not cause damage to a user
  682. session.
  683. f. Software engineering.
  684.  
  685.  
  686.  
  687. The verification system shall be implemented using documented
  688. software engineering practices.  The software shall be internally
  689. structured into well-defined, independent modules for ease of
  690. maintainability and configuration management. 
  691. g. Logical theory.
  692.  
  693.  
  694.  
  695. All logical theories used in the verification system shall be
  696. sound.  If more than one logical theory is used in the verification
  697. system, then there shall be evidence that the theories work together
  698. via a metalogic.  This provides the users with a sound method
  699. of interaction among the theories.
  700. h. Machine independence.
  701.  
  702.  
  703.  
  704. The functioning of the methodology and the language of the verification
  705. system shall be machine independent.  This is to ensure that the
  706. functioning of the theory, specification language, reasoning mechanism
  707. and other essential features does not change from one machine
  708. to another.  Additionally, the responses that the user receives
  709. from each of the components of the verification system should
  710. be consistent across the different hardware environments that
  711. support the verification system.
  712. 3.4 DOCUMENTATION
  713.  
  714. a. Informal justification.
  715.  
  716.  
  717.  
  718. An informal justification of the methodology behind the verification
  719. system shall be provided.  All parts of the methodology must be
  720. fully documented to serve as a medium for validating the accuracy
  721. of the stated implementation of the verification system.  The
  722. logical theory used in the verification system shall be documented.
  723.  If more than one logical theory exists in the system, the metalogic
  724. employed in the system shall be explained and fully documented.
  725.  This documentation is essential for the evaluators and will aid
  726. the users in understanding the methodology.
  727. b. Formal definition.
  728.  
  729.  
  730.  
  731. A formal definition (e.g., denotational semantics) of the specification
  732. language(s) shall be provided.  A formal definition shall include
  733. a clear semantic definition of the expressions supported by the
  734. specification language and a concise description of the syntax
  735. of all specification language constructs.  This is essential for
  736. the evaluators and will aid the users in understanding the specification
  737. language.
  738. c. Explanation of methodology.
  739.  
  740.  
  741.  
  742. A description of how to use the methodology, its tools, its limitations,
  743. and the kinds of properties that it can verify shall be provided.
  744.  This is essential for users to be able to understand the methodology
  745. and to use the verification system effectively.
  746. 4. IMPLEMENTATION AND OTHER SUPPORT FACTORS
  747.  
  748.  
  749.  
  750. The NCSC considers the support factors listed in this section
  751. to be measures of the usefulness, understandability, and maintainability
  752. of the verification system.  The support factors are divided into
  753. the following three categories:  1) features, 2) assurances, and
  754. 3) documentation.
  755.  
  756.  
  757. Two features that provide support for the user are the interface
  758. and the base hardware of the verification system.  Configuration
  759. management, testing, and mainte*nance are three means of providing
  760. assurance.  (The Appendix contains additional information on configuration
  761. management.)  Documentation consists of a set of manuals and technical
  762. papers that fully describe the verification system, its components,
  763. application, operation, and maintenance.
  764. 4.1 FEATURES
  765.  
  766. 4.1.1 User Interface
  767.  
  768. a. Ease of use.
  769.  
  770.  
  771.  
  772. The interface for the verification system shall be user-friendly.
  773.  Input must be understandable, output must be informative, and
  774. the entire interface must support the users' goals.
  775. b. Understandable input.
  776.  
  777.  
  778.  
  779. Input shall be distinct and concise for each language construct
  780. and ade*quately represent what the system requires for the construct.
  781.  
  782. c. Understandable output.
  783.  
  784.  
  785.  
  786. Output from the components of the verification system shall be
  787. easily interpretable, precise, and consistent.  This is to ensure
  788. that users are provided with understandable and helpful information.
  789.  
  790. d. Compatibility.
  791.  
  792.  
  793.  
  794. Output from the screen, the processor, and the reasoning mechanism
  795. shall be compatible with their respective input, where appropriate.
  796.  It is reasonable for a specification processor (reasoning mechanism)
  797. to put assertions into a canonical form, but canonical forms should
  798. be compatible in the specification language (reasoning mechanism).
  799. e. Functionality.
  800.  
  801.  
  802.  
  803. The interface shall support the tasks required by the user to
  804. exercise the verification system effectively.  This is to ensure
  805. that all commands necessary to utilize the components of the methodology
  806. are available and functioning according to accompanying documentation.
  807. f. Error reporting.
  808.  
  809.  
  810.  
  811. The verification system shall detect, report, and recover from
  812. errors in a specification.  Error reporting shall remain consistent
  813. by having the same error message generated each time the error
  814. identified in the message is encountered.  The output must be
  815. informative and interpretable by the users.
  816.  
  817.  
  818. Hardware Support  
  819. 4.1.2 Hardware Support
  820.  
  821. a. Availability.
  822.  
  823.  
  824.  
  825. The verification system shall be available on commonly used computer
  826. systems.  This will help ensure that users need not purchase expensive
  827. or outdated machines, or software packages to run the verification
  828. system.
  829. b. Efficiency.
  830.  
  831.  
  832.  
  833. Processing efficiency and memory usage shall be reasonable for
  834. specifications of substantial size.  This ensures that users are
  835. able to process simple (no complex constructs), short (no more
  836. than two or three pages) specifications in a reasonable amount
  837. of time (a few minutes).  The processing time of larger, more
  838. complex specifications shall be proportional to the processing
  839. time of smaller, less complex specifications.  Users should not
  840. need to wait an unacceptable amount of time for feedback.
  841. 4.2 ASSURANCE
  842.  
  843. 4.2.1 Configuration Management
  844.  
  845. a. Life-cycle maintenance.
  846.  
  847.  
  848.  
  849. Configuration management tools and procedures shall be used to
  850. track changes (both bug fixes and new features) to the verification
  851. system from initial concept to final implementation.  This provides
  852. both the system maintainers and the evaluators with a method of
  853. tracking the numerous changes made to the verification system
  854. to ensure that only sound changes are implemented.
  855. b. Configuration items.
  856.  
  857.  
  858.  
  859. Identification of Configuration Items (CIs) shall begin early
  860. in the design stage.  CIs are readily established on a logical
  861. basis at this time.  The configuration management process shall
  862. allow for the possibility that system changes will convert non-CI
  863. components into CIs.
  864. c. Configuration management tools.
  865.  
  866.  
  867.  
  868. Tools shall exist for comparing a newly generated version with
  869. the pre*vious version.  These tools shall confirm that a) only
  870. the intended changes have been made in the code that will actually
  871. be used as the new version of the verification system, and b)
  872. no additional changes have been inserted into the verification
  873. system that were not intended by the system developer.  The tools
  874. used to perform these functions shall also be under strict configuration
  875. control. 
  876. d. Configuration control.
  877.  
  878.  
  879.  
  880. Configuration control shall cover a broad range of items including
  881. software, documentation, design data, source code, the running
  882. version of the object code, and tests.  Configuration control
  883. shall begin in the earliest stages of design and development and
  884. extend over the full life of the CIs.  It involves not only the
  885. approval of changes and their implementation but also the updat*ing
  886. of all related material to reflect each change.  For example,
  887. often a change to one area of a verification system may necessitate
  888. a change to an*other area.  It is not acceptable to write or update
  889. documentation only for new code or newly modified code, rather
  890. than for all parts of the verification sys*tem affected by the
  891. addition or change.  Changes to all CIs shall be subject to review
  892. and approval.
  893.  
  894.  
  895. The configuration control process begins with the documentation
  896. of a change request.  This change request should include justification
  897. for the proposed change, all of the affected items and documents,
  898. and the proposed solution.  The change request shall be recorded
  899. in order to provide a way of tracking all proposed system changes
  900. and to ensure against duplicate change requests being processed.
  901. e. Configuration accounting.
  902.  
  903.  
  904.  
  905. Configuration accounting shall yield information that can be used
  906. to answer the following questions:  What source code changes were
  907. made on a given date?  Was a given change absolutely necessary?
  908.  Why or why not?  What were all the changes in a given CI between
  909. releases N and N+1?  By whom were they made, and why?  What other
  910. modifications were required by the changes to this CI?  Were modifications
  911. required in the test set or documentation to accommodate any of
  912. these changes?  What were all the changes made to support a given
  913. change request?
  914. f. Configuration auditing.
  915.  
  916.  
  917.  
  918. A configuration auditor shall be able to trace a system change
  919. from start to finish.  The auditor shall check that only approved
  920. changes have been implemented, and that all tests and documentation
  921. have been updated concurrently with each implementation to reflect
  922. the current status of the system.
  923. g. Configuration control board.
  924.  
  925.  
  926.  
  927. The vendor's Configuration Control Board (CCB) shall be responsible
  928. for approving and disapproving change requests, prioritizing approved
  929. modifications, and verifying that changes are properly incorporated.
  930.  The members of the CCB shall interact periodically to discuss
  931. configuration man*agement topics such as proposed changes, configuration
  932. status accounting reports, and other topics that may be of interest
  933. to the different areas of the system development.
  934.  
  935.  
  936. Support and Maintenance
  937. 4.2.2 Support and Maintenance
  938.  
  939.  
  940.  
  941. The verification system shall have ongoing support and maintenance
  942. from the developers or another qualified vendor.  Skilled maintainers
  943. are necessary to make changes to the verification system. 
  944.  
  945.  
  946. Testing 
  947. 4.2.3 Testing
  948.  
  949. a. Functional tests.
  950.  
  951.  
  952.  
  953. Functional tests shall be conducted to demonstrate that the verification
  954. system operates as advertised.  These tests shall be maintained
  955. over the life cycle of the verification system.  This ensures
  956. that a test suite is available for use on all versions of the
  957. verification system.  The test suite shall be enhanced as software
  958. errors are identified to demonstrate the elimination of the errors
  959. in subsequent versions.  Tests shall be done at the module level
  960. to demonstrate compliance with design documentation and at the
  961. system level to demonstrate that software accurately generates
  962. assertions, correctly implements the logic, and correctly responds
  963. to user commands. 
  964. b. Stress testing.
  965.  
  966.  
  967.  
  968. The system shall undergo stress testing by the evaluation team
  969. to test the limits of and to attempt to generate contradictions
  970. in the specification language, the reasoning mechanism, and large
  971. specifications.
  972. 4.3 DOCUMENTATION
  973.  
  974. a. Configuration management plan.
  975.  
  976.  
  977.  
  978. A configuration management plan and supporting evidence assuring
  979. a consistent mapping of documentation and tools shall be provided
  980. for the evaluation.  This provides the evaluators with evidence
  981. that compatibility exists between the components of the verification
  982. system and its documentation.  The plan shall include the following:
  983.  
  984.  • 1. The configuration management plan shall describe what is
  985. to be done to implement configuration management in the verification
  986. system.  It shall define the roles and responsibilities of designers,
  987. developers, management, the Configuration Control Board, and all
  988. of the personnel involved with any part of the life cycle of the
  989. verification system. 
  990.  • 2. Tools used for configuration management shall be documented
  991. in the configuration management plan.  The forms used for change
  992. control, conventions for labeling configuration items, etc., shall
  993. be contained in the configuration management plan along with a
  994. description of each.
  995.  • 3. The plan shall describe procedures for how the design and
  996. implementation of changes are proposed, evaluated, coordinated,
  997. and approved or disapproved.  The configuration management plan
  998. shall also include the steps to ensure that only those approved
  999. changes are actually included and that the changes are included
  1000. in all of the necessary areas.
  1001.  • 4. The configuration management plan shall describe how changes
  1002. are made to the plan itself and how emergency procedures are handled.
  1003.  It should describe the procedures for performing time-sensitive
  1004. changes without going through a full review process.  These procedures
  1005. shall define the steps for retroactively implementing configuration
  1006. management after the emergency change has been completed.
  1007.  
  1008.  
  1009.  
  1010.  
  1011.  
  1012. b. Configuration management evidence.
  1013.  
  1014.  
  1015.  
  1016. Documentation of the configuration management activities shall
  1017. be provided to the evaluators.  This ensures that the policies
  1018. of the configuration management plan have been followed.
  1019. c. Source code.
  1020.  
  1021.  
  1022.  
  1023. Well-documented source code for the verification system, as well
  1024. as documentation to aid in analysis of the code during the evaluation,
  1025. shall be provided.  This provides the evaluators with evidence
  1026. that good software engineering practices and configuration management
  1027. procedures were used in the implementation of the verification
  1028. system.
  1029. d. Test documentation.
  1030.  
  1031.  
  1032.  
  1033. Documentation of test suites and test procedures used to check
  1034. functionality of the system shall be provided.  This provides
  1035. an explanation to the evaluators of each test case, the testing
  1036. methodology, test results, and procedures for using the tests.
  1037. e. User's guide.
  1038.  
  1039.  
  1040.  
  1041. An accurate and complete user's guide containing all available
  1042. commands and their usage shall be provided in a tutorial format.
  1043.  The user's guide shall contain worked examples.  This is necessary
  1044. to guide the users in the use of the verification system.
  1045. f. Reference manuals.
  1046.  
  1047.  
  1048.  
  1049. A reference manual that contains instructions, error messages,
  1050. and examples of how to use the system shall be provided.  This
  1051. provides the users with a guide for problem-solving techniques
  1052. as well as answers to questions that may arise while using the
  1053. verification system.
  1054. g. Facilities manual.
  1055.  
  1056.  
  1057.  
  1058. A description of the major components of the software and their
  1059. interfacing shall be provided.  This will provide users with a
  1060. limited knowledge of the hardware base required to configure and
  1061. use the verification system.
  1062. h. Vendor report.
  1063.  
  1064.  
  1065.  
  1066. A report written by the vendor during a reevaluation that provides
  1067. a complete description of the verification system and changes
  1068. made since the initial evaluation shall be provided.  This report,
  1069. along with configuration management documentation, provides the
  1070. evaluators with evidence that soundness of the system has not
  1071. been jeopardized.
  1072. i. Significant worked examples.
  1073.  
  1074.  
  1075.  
  1076. Significant worked examples shall be provided which demonstrate
  1077. the strengths, weaknesses, and limitations of the verification
  1078. system.  These examples shall reflect portions of computing systems.
  1079.  They may reside in the user's guide, the reference manual, or
  1080. a separate document.
  1081. 5. FUTURE DIRECTIONS
  1082.  
  1083.  
  1084.  
  1085. The purpose of this section is to list possible features for future
  1086. or beyond-A1 verification systems.  Additionally, it contains
  1087. possibilities for future research-areas that researchers may choose
  1088. to investigate.  Research and development of new verification
  1089. systems or investigating areas not included in this list is also
  1090. encouraged.  Note that the order in which these items appear has
  1091. no bearing on their relative importance.
  1092.  
  1093.  • a. The specification language should permit flexibility in
  1094. approaches to specification.
  1095.  • b. The specification language should allow the expression
  1096. of properties involving liveness, concurrency, and eventuality.
  1097.  • c. The reasoning mechanism should include a method for reasoning
  1098. about information flows.
  1099.  • d. The design and code of the verification system should be
  1100. formally verified.
  1101.  • e. The theory should support rapid prototyping.  Rapid prototyping
  1102. supports a way of developing a first, quick version of a specification.
  1103.  The prototype provides immediate feedback to the user.
  1104.  • f. The verification system should make use of standard (or
  1105. reusable) components where possible (for example, use of a standard
  1106. windowing system, use of a standard language-independent parser,
  1107. editor, or printer, use of a standard database support system,
  1108. etc.).
  1109.  • g. The verification system should provide a language-specific
  1110. verifier for a commonly used systems programming language.
  1111.  • h. The verification system should provide a method for mapping
  1112. a top-level specification to verified source code.
  1113.  • i. The verification system should provide a tool for automatic
  1114. test data generation of the design specification.
  1115.  • j. The verification system should provide a means of identifying
  1116. which paths in the source code of the verification system are
  1117. tested by a test suite.
  1118.  • k. The verification system should provide a facility for high-level
  1119. debugging/tracing of unsuccessful proofs.
  1120.  • l. A formal justification of the methodology behind the verification
  1121. system should be provided.
  1122.  
  1123.  
  1124.  
  1125.  
  1126.  
  1127. APPENDIX
  1128.  
  1129. CONFIGURATION MANAGEMENT
  1130.  
  1131.  
  1132.  
  1133. The purpose of configuration management is to ensure that changes
  1134. made to verification systems take place in an identifiable and
  1135. controlled environment.  Configuration managers take responsibility
  1136. that additions, deletions, or changes made to the verification
  1137. system do not jeopardize its ability to satisfy the requirements
  1138. in Chapters 3 and 4.  Therefore, configuration management is vital
  1139. to maintaining the endorsement of a verification system.
  1140.  
  1141.  
  1142. Additional information on configuration management can be found
  1143. in A Guide to Understanding Configuration Management in Trusted
  1144. Systems. [3]
  1145. OVERVIEW OF CONFIGURATION MANAGEMENT
  1146.  
  1147.  
  1148.  
  1149. Configuration management is a discipline applying technical and
  1150. administrative direction to:  1) identify and document the functional
  1151. and physical characteristics of each configuration item for the
  1152. system; 2) manage all changes to these characteristics; and 3)
  1153. record and report the status of change processing and implementation.
  1154.  Configuration management involves process monitoring, version
  1155. control, information capture, quality control, bookkeeping, and
  1156. an organizational framework to support these activities.  The
  1157. configuration being managed is the verification system plus all
  1158. tools and documentation related to the configuration process.
  1159.  
  1160.  
  1161. Four major aspects of configuration management are configuration
  1162. identification, configuration control, configuration status accounting,
  1163. and configuration auditing. 
  1164. CONFIGURATION IDENTIFICATION
  1165.  
  1166.  
  1167.  
  1168. Configuration management entails decomposing the verification
  1169. system into identifi*able, understandable, manageable, trackable
  1170. units known as Configuration Items (CIs).  A CI is a uniquely
  1171. identifiable subset of the system that represents the small*est
  1172. portion to be subject to independent configuration control procedures.
  1173.  The decomposition process of a verification system into CIs is
  1174. called configuration identification. 
  1175.  
  1176.  
  1177. CIs can vary widely in size, type, and complexity.  Although there
  1178. are no hard-and-fast rules for decomposition, the granularity
  1179. of CIs can have great practical importance.  A favorable strategy
  1180. is to designate relatively large CIs for elements that are not
  1181. expected to change over the life of the system, and small CIs
  1182. for elements likely to change more frequently. 
  1183. CONFIGURATION CONTROL
  1184.  
  1185.  
  1186.  
  1187. Configuration control is a means of assuring that system changes
  1188. are approved before being implemented, only the proposed and approved
  1189. changes are implemented, and the implementation is complete and
  1190. accurate.  This involves strict procedures for proposing, monitoring,
  1191. and approving system changes and their implementation.  Configuration
  1192. control entails central direction of the change process by personnel
  1193. who coordinate analytical tasks, approve system changes, review
  1194. the implementation of changes, and supervise other tasks such
  1195. as documentation.
  1196. CONFIGURATION ACCOUNTING
  1197.  
  1198.  
  1199.  
  1200. Configuration accounting documents the status of configuration
  1201. control activities and in general provides the information needed
  1202. to manage a configuration effectively.  It allows managers to
  1203. trace system changes and establish the history of any developmental
  1204. problems and associated fixes.  Configuration accounting also
  1205. tracks the status of current changes as they move through the
  1206. configuration control process.  Configuration accounting establishes
  1207. the granularity of recorded information and thus shapes the accuracy
  1208. and usefulness of the audit function.
  1209.  
  1210.  
  1211. The accounting function must be able to locate all possible versions
  1212. of a CI and all of the incremental changes involved, thereby deriving
  1213. the status of that CI at any specific time.  The associated records
  1214. must include commentary about the reason for each change and its
  1215. major implications for the verification system.
  1216. CONFIGURATION AUDIT
  1217.  
  1218.  
  1219.  
  1220. Configuration audit is the quality assurance component of configuration
  1221. management.  It involves periodic checks to determine the consistency
  1222. and completeness of accounting information and to verify that
  1223. all configuration management policies are being followed.  A vendor's
  1224. configuration management program must be able to sustain a complete
  1225. configuration audit by an NCSC review team.
  1226. CONFIGURATION MANAGEMENT PLAN
  1227.  
  1228.  
  1229.  
  1230. Strict adherence to a comprehensive configuration management plan
  1231. is one of the most important requirements for successful configuration
  1232. management.  The configuration management plan is the vendor's
  1233. document tailored to the company's practices and personnel.  The
  1234. plan accurately describes what the vendor is doing to the system
  1235. at each moment and what evidence is being recorded. 
  1236. CONFIGURATION CONTROL BOARD
  1237.  
  1238.  
  1239.  
  1240. All analytical and design tasks are conducted under the direction
  1241. of the vendor's corporate entity called the Configuration Control
  1242. Board (CCB).  The CCB is headed by a chairperson who is responsible
  1243. for assuring that changes made do not jeopardize the soundness
  1244. of the verification system.  The Chairperson assures that the
  1245. changes made are approved, tested, documented, and implemented
  1246. correctly. 
  1247.  
  1248.  
  1249. The members of the CCB should interact periodically, either through
  1250. formal meetings or other available means, to discuss configuration
  1251. management topics such as proposed changes, configuration status
  1252. accounting reports, and other topics that may be of interest to
  1253. the different areas of the system development.  These interactions
  1254. should be held to keep the entire system team updated on all advancements
  1255. or alterations in the verification system.
  1256. GLOSSARY
  1257.  
  1258. Beta Version
  1259.  
  1260.  
  1261.  
  1262. Beta versions are intermediate releases of a product to be tested
  1263. at one or more customer sites by the software end-user.  The customer
  1264. describes in detail any problems encountered during testing to
  1265. the developer, who makes the appropriate modifications.  Beta
  1266. versions are not endorsed by the NCSC, but are primarily used
  1267. for debugging and testing prior to submission for endorsement.
  1268. Complete
  1269.  
  1270.  
  1271.  
  1272. A theory is complete if and only if every sentence of its language
  1273. is either provable or refutable.
  1274. Concurrency 
  1275.  
  1276.  
  1277.  
  1278. Simultaneous or parallel processing of events.
  1279. Configuration Accounting -
  1280.  
  1281.  
  1282.  
  1283.  The recording and reporting of configuration item descriptions
  1284. and all departures from the baseline during design and production.
  1285. Configuration Audit
  1286.  
  1287.  
  1288.  
  1289. An independent review of computer software for the purpose of
  1290. assessing compliance with established requirements, standards,
  1291. and baselines. [3]
  1292. Configuration Control
  1293.  
  1294.  
  1295.  
  1296. The process of controlling modifications to the system's design,
  1297. hardware, firmware, software, and documentation which provides
  1298. sufficient assurance that the system is protected against the
  1299. introduction of improper modification prior to, during, and after
  1300. system implementation. [3] Configuration Control Board (CCB) An
  1301. established vendor committee that is the final authority on all
  1302. proposed changes to the verification system.
  1303. Configuration Identification 
  1304.  
  1305.  
  1306.  
  1307. The identifying of the system configuration throughout the design,
  1308. development, test, and production tasks. [3]
  1309. Configuration Item (CI) 
  1310.  
  1311.  
  1312.  
  1313. The smallest component tracked by the configuration management
  1314. system. [3]
  1315. Configuration Management
  1316.  
  1317.  
  1318.  
  1319. The process of controlling modifications to a verification system,
  1320. including documentation, that provides sufficient assurance that
  1321. the system is protected against the introduction of improper modification
  1322. before, during, and after system implementation. 
  1323. Conjecture
  1324.  
  1325.  
  1326.  
  1327. A general conclusion proposed to be proved upon the basis of certain
  1328. given premises or assumptions.
  1329. Consistency (Mathematical)
  1330.  
  1331.  
  1332.  
  1333. A logical theory is consistent if it contains no formula such
  1334. that the formula and its negation are provable theorems.
  1335. Consistency (Methodological)
  1336.  
  1337.  
  1338.  
  1339. Steadfast adherence to the same principles, course, form, etc.
  1340. Correctness
  1341.  
  1342.  
  1343.  
  1344. Free from errors; conforming to fact or truth.
  1345.  
  1346.  
  1347. Correctness
  1348.  
  1349.  
  1350.  Conditions
  1351. Conjectures 
  1352.  
  1353.  
  1354.  
  1355. that formalize the rules, security policies, models, or other
  1356. critical requirements on a system.
  1357. Design Verification
  1358.  
  1359.  
  1360.  
  1361. A demonstration that a formal specification of a software system
  1362. satisfies the correctness conditions (critical requirements specification).
  1363. Documentation
  1364.  
  1365.  
  1366.  
  1367. A set of manuals and technical papers that fully describe the
  1368. verification system, its components, application, and operation.
  1369. Endorsed Tools List (ETL)
  1370.  
  1371.  
  1372.  
  1373. A list composed of those verification systems currently recommended
  1374. by the NCSC for use in developing highly trusted systems.
  1375. Eventuality
  1376.  
  1377.  
  1378.  
  1379. The ability to prove that at some time in the future, a particular
  1380. event will occur.
  1381. Formal Justification
  1382.  
  1383.  
  1384.  
  1385. Mathematically precise evidence that the methodology of the verification
  1386. system is sound.
  1387. Formal Verification
  1388.  
  1389.  
  1390.  
  1391. The process of using formal proofs to demonstrate the
  1392.  
  1393.  
  1394. consistency (design verification) between a formal specification
  1395. of a
  1396.  
  1397.  
  1398. system and a formal security policy model or (implementation verification)
  1399.  
  1400.  
  1401. between the formal specification and its program implementation.
  1402. [1]
  1403. Implementation Verification
  1404.  
  1405.  
  1406.  
  1407. A demonstration that a program implementation satisfies a formal
  1408. specification of a system.
  1409. Informal Justification
  1410.  
  1411.  
  1412.  
  1413. An English description of the tools of a verification system and
  1414. how they interact.  This includes a justification of the soundness
  1415. of the theory.
  1416. Language
  1417.  
  1418.  
  1419.  
  1420. A set of symbols and rules of syntax regulating the relationship
  1421. between the symbols, used to convey information.
  1422. Liveness
  1423.  
  1424.  
  1425.  
  1426. Formalizations that ensure that a system does something that it
  1427. should do.
  1428. Metalogic
  1429.  
  1430.  
  1431.  
  1432. A type of logic used to describe another type of logic or a combination
  1433. of different types of logic.
  1434. Methodology
  1435.  
  1436.  
  1437.  
  1438. The underlying principles and rules of organization of a verification
  1439. system.
  1440. Production Quality Verification System
  1441.  
  1442.  
  1443.  
  1444. A verification system that is sound, user-friendly,
  1445.  
  1446.  
  1447. efficient, robust, well-documented, maintainable, well-engineered
  1448.  
  1449.  
  1450. (developed with software engineering techniques), available on
  1451. a variety
  1452.  
  1453.  
  1454. of hardware, and promoted (has education available for users).
  1455. [2]
  1456. Proof
  1457.  
  1458.  
  1459.  
  1460. A syntactic analysis performed to validate the truth of an assertion
  1461. relative to an (assumed) base of assertions.
  1462. Proof Checker
  1463.  
  1464.  
  1465.  
  1466. A tool that 1) accepts as input an assertion (called a conjecture),
  1467. a set of assertions (called assumptions), and a proof; 2) terminates
  1468. and outputs either success or failure; and 3) if it succeeds,
  1469. then the conjecture is a valid consequence of the assumptions.
  1470. Reasoning Mechanism
  1471.  
  1472.  
  1473.  
  1474. A tool (interactive or fully automated) capable of checking or
  1475. constructing proofs.
  1476. Safety Properties
  1477.  
  1478.  
  1479.  
  1480. Formalizations that ensure that a system does not do something
  1481. that it should not do.
  1482. Semantics
  1483.  
  1484.  
  1485.  
  1486. A set of rules for interpreting the symbols and well-formed formulae
  1487. of a language.
  1488. Sound
  1489.  
  1490.  
  1491.  
  1492. An argument is sound if all of its propositions are true and its
  1493. argument form is valid.  A proof system is sound relative to a
  1494. given semantics if every conjecture that can be proved is a valid
  1495. consequence of the assumptions used in the proof.
  1496. Specification Language
  1497.  
  1498.  
  1499.  
  1500. A logically precise language used to describe the structure or
  1501. behavior of a system to be verified.
  1502. Specification Processor
  1503.  
  1504.  
  1505.  
  1506. A software tool capable of receiving input, parsing it, generating
  1507. conjectures (candidate theorems), and supplying results for further
  1508. analysis (e.g., reasoning mechanism).
  1509. Syntax
  1510.  
  1511.  
  1512.  
  1513. A set of rules for constructing sequences of symbols from the
  1514. primitive symbols of a language.
  1515.  
  1516.  
  1517. Technical Assessment Report (TAR)
  1518.  
  1519.  
  1520. A report that is written by an evaluation team during an evaluation
  1521. of a verification system and available upon completion.
  1522. Theorem
  1523.  
  1524.  
  1525.  
  1526. In a given logical system, a well-formed formula that is proven
  1527. in that system.
  1528. Theory
  1529.  
  1530.  
  1531.  
  1532. A formal theory is a coherent group of general propositions used
  1533. as principles of explanation for a particular class of phenomena.
  1534. User-Friendly
  1535.  
  1536.  
  1537.  
  1538. A system is user-friendly if it facilitates learning and usage
  1539. in an efficient manner.
  1540. Valid
  1541.  
  1542.  
  1543.  
  1544. An argument is valid when the conclusion is a valid consequence
  1545. of the assumptions used in the argument.
  1546. Vendor Report (VR)
  1547.  
  1548.  
  1549.  
  1550. A report that is written by a vendor during and available upon
  1551. completion of a reevaluation of a verification system.
  1552. Verification
  1553.  
  1554.  
  1555.  
  1556. The process of comparing two levels of system specification for
  1557. proper correspondence (e.g., security policy model with top-level
  1558. specification, top-level specification with source code, or source
  1559. code with object code).  This process may or may not be automated.
  1560.  
  1561.  
  1562. [1]
  1563. Verification Committee
  1564.  
  1565.  
  1566.  
  1567. A standing committee responsible for the management of the verification
  1568. efforts at the NCSC.  The committee is chaired by the NCSC Deputy
  1569. Director and includes the NCSC Chief Scientist, as well as representatives
  1570. from both the NCSC's Office of Research and Development and Office
  1571. of Computer Security Evaluations, Publications, and Support.
  1572. Verification System
  1573.  
  1574.  
  1575.  
  1576. An integrated set of tools and techniques for performing verification.
  1577. Well-Formed Formula
  1578.  
  1579.  
  1580.  
  1581. A sequence of symbols from a language that is constructed in accordance
  1582. with the syntax for that language.
  1583. BIBLIOGRAPHY
  1584.  
  1585.  
  1586.  
  1587. [1]  Department of Defense, Department of Defense Trusted Computer
  1588. System Evaluation Criteria, DOD 5200.28-STD, December 1985. 
  1589.  
  1590.  
  1591. [2] Kemmerer, Richard A., Verification Assessment Study Final
  1592. Report, University of California, March 1986.
  1593.  
  1594.  
  1595. [3] National Computer Security Center, A Guide to Understanding
  1596. Configuration Management in Trusted Systems, NCSC-TG-006, March
  1597. 1988.
  1598.  
  1599.  
  1600. [4] National Computer Security Center, Trusted Network Interpretation
  1601. of the Trusted Computer System Evaluation Criteria, NCSC-TG-005,
  1602. July 1987.
  1603.  
  1604.  
  1605. [5] National Security Agency, Information Systems Security Products
  1606. and Services Catalogue, Issued Quarterly, January 1989 and successors.
  1607.  
  1608.  
  1609.  
  1610.